(* $Id: simplifyPrinter.ml 131 2007-10-29 09:01:06Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

module B = Buffer
open Pprint
open PprintExt
open PFOLSyntax.Raw

let id_text x = 
  text (Demangle.str x)

let kw x = 
  text x

let sym x =
  text x

let pid x = 
  text (PIdentifier.as_string x)

let tid x = 
  text (PIdentifier.as_string x)

let indent t = 
  hang 2 (group t)
    
let fresh_counter = ref 0

let rec name_from_int i : string =
  if i < 26 then
    String.make 1 (Char.chr (0x61 + i))
  else
    String.concat "_" [ name_from_int (i / 26 - 1) ; name_from_int (i mod 26) ]

let init_fresh () = 
  fresh_counter := 0

let fresh () = 
  incr fresh_counter;
  !fresh_counter

let fresh_type_id _ =
  tid (PIdentifier.mk_type_id (Position.dummy, 
			      "'" ^ name_from_int (fresh ())))

module IntSet = Set.Make (struct type t = int
				 let compare = compare 
			  end)

let used_tuples = ref IntSet.empty 

let tuple_name i = 
  Printf.sprintf "tuple%d" i

let tuple i = 
  used_tuples := IntSet.add i !used_tuples;
  tuple_name i

let tuple_type i = 
  let vs = Misc.repeat i fresh_type_id in
  let d = comma_sep vs in
    d ++ sym "->" ++ paren d ++ text (tuple i)
      
let tuple_type_declaration i = 
  let vs = Misc.repeat i fresh_type_id in
    kw "type" ++ paren (comma_sep vs) ++ text (tuple_name i)

let declare_tuple i ds = 
  ((tuple_type_declaration i $$
      kw "logic " ++ text (tuple_name i) ++ sym ":" ++ tuple_type i)
  ) :: ds

let declare_tuples () = 
  vcat (IntSet.fold declare_tuple !used_tuples [])

let fresh_axiom_id _ =
  pid (PIdentifier.mk_predicate_id (Position.dummy, 
				    (Printf.sprintf "property_%d" (fresh ()))))

let mark_as_universal rs v = 
  PIdentifier.Set.add v rs

let mark_as_universals rs vs = 
  List.fold_left mark_as_universal rs vs

let is_universal v rs =
  (PIdentifier.Set.mem v rs)

let empty_rs = PIdentifier.Set.empty

let rec quantified q quantifier ts body t = 
  match ts with
    | [] -> body t
    | v :: ts ->
	group (paren (kw q ++ paren (quantifier v) 
			$$ group (quantified q quantifier ts body t)))

let rec predicate rs p = 
  match p with
    | Forall (bs, ts, p) ->
	quantified "FORALL" (binding rs) bs (predicate rs) p
	  
    | Exists (bs, p) ->
	quantified "EXISTS" (binding rs) bs (predicate rs) p
	  
    | LogicBinOpApp (op, lhs, rhs) ->
	group (paren (binop op ++ predicate rs lhs ++ predicate rs rhs))

    | BinOpApp (op, lhs, rhs) ->
	group (paren (binop op ++ term lhs ++ term rhs))
	  
    | Neg p ->
	paren (kw "NOT" ++ predicate rs p)
	 
    | PApp (p, []) ->
	paren (id p)
 
    | PApp (p, ts) ->
	paren (id p ++ space_sep' term ts)
	  
    | PEq (lhs, rhs) ->
	paren (kw "EQ" ++ term lhs ++ term rhs)
	  
    | PTrue ->
	kw "TRUE"
	  
    | PFalse ->
	kw "FALSE"
	  
    | Pre (f, t, u) ->
	paren (kw "pre" ++ space_sep [id f; term t; term u ])
	  
    | Post (f, t1, t2, t3) ->
	paren (kw "post" ++ space_sep [id f; term t1; term t2; term t3 ])

    | Reify t ->
	paren (kw "reify" ++ term t)

    | _ -> 
	assert false


and ipredicate rs p = 
  indent (predicate rs p)

and binop = function
  | Conj -> kw "AND"
  | Disj -> kw "OR"
  | Imply -> kw "IMPLIES"
  | Equiv -> kw "IFF"
  | LessThan -> kw "<"
  | LessEqualThan -> kw "<="
  | GreaterThan -> kw ">"
  | GreaterEqualThan -> kw ">="
	
and binding rs (x, ty) =
  id x

and term = function
  | Var x -> 
      id x

  | App (f, ts) -> 
      paren (id f ++ space_sep' term ts)

  | Prod [] ->
      text "void"

  | Prod [ t ] ->
      term t
	
  | Prod ts -> 
      paren (text (tuple (List.length ts)) ++ space_sep' term ts)

  | Prim p ->
      primitive p

  | PrimApp (p, [ t1; t2 ]) ->
      paren (term_binop p ++ term t1 ++ term t2)

  | PredObjectApp (p, ts) ->
      paren (text "apply" ++ space_sep [ term p; term (Prod ts) ])

  | _ -> 
      assert false

and term_binop = function
  | PAdd -> 
      sym "+"

  | PSub ->
      sym "-"

  | PMult ->
      sym "*"

  | PDiv ->
      sym "/"

  | _ -> 
      assert false


and primitive = function
  | PInt x ->
      text (string_of_int x)

  | PTrueBool ->
      text "true"

  | PFalseBool ->
      text "false"

  | PLessThanObj ->
      text "less_than_object"

  | PGreaterThanObj ->
      text "greater_than_object"

  | PLessEqualThanObj ->
      text "less_equal_than_object"

  | PGreaterEqualThanObj ->
      text "greater_equal_than_object"

  | PEqObj ->
      text "equal_obj"

  | _ -> 
      assert false

and names_from_predicate_type_scheme (vs, tys) = 
  space_sep (Misc.list_mapi (fun i _ -> text ("ARG" ^ (string_of_int i))) tys)
	    
and bindings rs bs = 
  space_sep' (binding rs) bs


and declaration = function
  | DVal (v, ts) -> 
(*      paren (kw "BG_PUSH" ++ id v)*)
      empty

  | DPred (p, PredDec s) ->
      paren (kw "DEFPRED" 
	     ++ paren (id p ++ names_from_predicate_type_scheme s))

  | DPred (p, PredDef (vs, bs, def)) ->
      paren (kw "DEFPRED" 
	     ++ paren (id p ++ bindings empty_rs bs)
	     ++ ipredicate empty_rs def)
	  
  | DAxiom (vs, f) ->
      paren (kw "BG_PUSH" ++ ipredicate empty_rs f)

  | _ ->
      empty
	
and query = function
  | EmptyQuery ->
      (empty, [])
	
  | ConsGoal (p, q) -> 
      let q, gs = query q in
      let g = predicate empty_rs p in
	(g, g :: gs)

  | ConsDecl (d, q) ->
      let q, gs = query q in
	((declaration d $$ q), gs)

and id t = 
  id_text (PIdentifier.as_string t)

let as_string d = 
  let b = B.create 13 in
    Buffer.pretty 0.6 120 b d;
    B.contents b  

let prologue = 
  empty 
    $$ paren (kw "DEFPRED" ++ text "(pre X Y Z)")
    $$ paren (kw "DEFPRED" ++ text "(post X Y Z U)")
    $$ paren (kw "DEFPRED" ++ text "(reify X)")

let print p = 
  init_fresh ();
  let d, g = query p in
    (as_string (prologue $$ d), String.concat "\n" (List.map as_string g))


